GermanWikipedia - /page/entry.mu

<!DOCTYPE html>

<title>Computation Tree Logic</title>

</head>

<h1 id="firstHeading" class="firstHeading mw-first-heading">Computation Tree Logic</h1>

</header>

</div>

Die Computation Tree Logic (kurz CTL) ist eine <a href="Temporale_Logik" title="Temporale Logik">temporale Logik</a>, deren Modell der Zeit eine baumartige Struktur hat. Die zeitliche Änderung von Zuständen und deren Eigenschaften wird durch Pfade innerhalb dieser Baumstruktur modelliert. Hierbei hat die Zukunft mehrere Pfade, wobei nicht festgelegt ist, welche letztendlich realisiert werden. Demnach können Aussagen über die mögliche Entwicklungen getroffen werden.

Die CTL wird zur <a href="Verifizierung" title="Verifizierung">Verifikation</a> von Hard- und Software verwendet, üblicherweise von <a href="Model_Checking" title="Model Checking">Model Checkern</a>.

Zu der Familie der temporalen Logiken gehört auch die <a href="Lineare_temporale_Logik" title="Lineare temporale Logik">linear temporale Logik</a> (LTL), wobei hier nur eine Zukunft möglich ist. Eine Verallgemeinerung der beiden Logiken wird als CTL* bezeichnet.

<div class="mw-heading mw-heading2"><h2 id="Syntax">Syntax</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Minimale_Grammatik">Minimale Grammatik</h3></div>

Sei <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle AP}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AP}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/0c5ad98caec3c0a2b988d988be2c78cd0dbfe442.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.489ex; height:2.176ex;" alt="{\displaystyle AP}" loading="lazy"> eine Menge von <a href="Aussage_(Logik)#Einfach_–_zusammengesetzt" title="Aussage (Logik)">atomaren Aussagen</a> (Behauptungen), dann ist jedes Element <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\in AP}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\in AP}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/990ea5e859d67389d3fb51ebc29ac94067accb63.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:7.588ex; height:2.509ex;" alt="{\displaystyle p\in AP}" loading="lazy"> eine CTL-Formel. Sind <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> und <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }" loading="lazy"> Formeln, dann auch <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d3977176cb0f5057b3dcc1cfeae7d80dcb9c9ee0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.936ex; height:2.509ex;" alt="{\displaystyle \neg \phi }" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi \lor \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi \lor \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/5092176ead49fad1831b66b924957541ea52f63a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.481ex; height:2.509ex;" alt="{\displaystyle \phi \lor \psi }" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\text{EX}}\phi }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\text{EX}}\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/cc7b35f5439d10d89e78725af5914bc76c6561d7.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.711ex; height:2.509ex;" alt="{\displaystyle {\text{EX}}\phi }" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\text{EG}}\phi }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\text{EG}}\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f59f96bbdc27967da501c87244a46398202db45e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.793ex; height:2.509ex;" alt="{\displaystyle {\text{EG}}\phi }" loading="lazy"> und <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi {\text{EU}}\psi }">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi {\text{EU}}\psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/89724096dbecfef397b61d8f2e4b9678c8cc959e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:6.225ex; height:2.509ex;" alt="{\displaystyle \phi {\text{EU}}\psi }" loading="lazy">. Dies definiert die minimale <a href="Formale_Grammatik" title="Formale Grammatik">Grammatik</a> von CTL. In der Regel wird diese allerdings um die gängigen <a href="Boolescher_Operator" title="Boolescher Operator">booleschen Operatoren</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \land }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \land }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d6823e5a222eb3ca49672818ac3d13ec607052c4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.55ex; height:2.009ex;" alt="{\displaystyle \land }" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \implies }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \implies }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/913c2e89ea94dfa446f69b056d4bf505e01fcc5f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.096ex; height:1.843ex;" alt="{\displaystyle \implies }" loading="lazy">und <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Leftrightarrow }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Leftrightarrow }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/64812e13399c20cf3ce94e049d3bb2d85f26abcf.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \Leftrightarrow }" loading="lazy">, sowie einigen weiteren temporalen Operatoren erweitert.

<div class="mw-heading mw-heading3"><h3 id="Temporale_Operatoren">Temporale Operatoren</h3></div>

Die Erweiterung der minimalen Grammatik um folgende Operatoren erhöht nicht die Mächtigkeit der <a href="Formale_Sprache" title="Formale Sprache">Sprache</a>, da alle Operatoren durch Umformungen zurückgeführt werden können.

<ul><li>Pfadoperatoren:

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c97018242fde2aa347a223776b48f19ce1174d52.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.129ex; height:2.509ex;" alt="{\displaystyle A\phi }" loading="lazy"> – auf allen Pfaden folgt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> (englisch: All)</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle E\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/908d8551927eec888cbf691afc865297994e0020.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.161ex; height:2.509ex;" alt="{\displaystyle E\phi }" loading="lazy"> – auf mindestens einem Pfad folgt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> (englisch: Exists)</li></ul></li>

<li>Pfad-spezifische Operatoren:

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle X\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/eadd604989b31949e09118cd56ca477b7cb234e9.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.365ex; height:2.509ex;" alt="{\displaystyle X\phi }" loading="lazy"> – unmittelbar folgt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> (englisch: neXt state)</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/02a8ecafdfba08456d0a44f369ccae6bb1c7c748.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.126ex; height:2.509ex;" alt="{\displaystyle F\phi }" loading="lazy"> – irgendwann folgt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> (englisch: some Future state oder Finally)</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle G\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/d9c4267cb29e4827f0d9b58883a5178ec472c29c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.212ex; height:2.509ex;" alt="{\displaystyle G\phi }" loading="lazy"> – auf dem folgenden Pfad folgt in jedem Zustand <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> (englisch: Globally)</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi U\psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/6e0693475b7aa333e7dd7aa5dae01d971f48a37b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.681ex; height:2.509ex;" alt="{\displaystyle \phi U\psi }" loading="lazy"> – <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> folgt bis zum Erreichen des Zustands <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }" loading="lazy"> (englisch: Until)</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi W\psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/5c8ca0470a56ac302dc17eab28cc848b96f59468.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.334ex; height:2.509ex;" alt="{\displaystyle \phi W\psi }" loading="lazy"> – <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> folgt immer oder bis zum Erreichen des Zustands <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }" loading="lazy"> (englisch: Weak Until)</li></ul></li></ul>

Pfad und pfad-spezifische Operatoren können miteinander kombiniert werden, sodass sich beispielsweise folgende Formeln ergeben:

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle EX\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1febfe4f3c6cd82fc8ba406129edf67012629332.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.141ex; height:2.509ex;" alt="{\displaystyle EX\phi }" loading="lazy"> – in (mind.) einem nächsten Zustand gilt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle EF\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/cfe60613cc75f89ec4355551aed514f651096a04.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.902ex; height:2.509ex;" alt="{\displaystyle EF\phi }" loading="lazy"> – in (mind.) einem der folgenden Zustände gilt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle EG\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4d40d6566e8928e7140644daea24f9be481b9e7c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.988ex; height:2.509ex;" alt="{\displaystyle EG\phi }" loading="lazy"> – es gibt (mind.) einen Pfad, so dass <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> entlang des ganzen Pfades gilt</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle E[\phi U\psi ]}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/24b321ed724e32428254de4b0399ab1336e7ddb1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.75ex; height:2.843ex;" alt="{\displaystyle E[\phi U\psi ]}" loading="lazy"> – es gibt einen Pfad, für den gilt: bis zum ersten Auftreten von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }" loading="lazy"> gilt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AX\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/a554a807375e83bcc0bfe9aa63b3d568811d0542.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.109ex; height:2.509ex;" alt="{\displaystyle AX\phi }" loading="lazy"> – in jedem nächsten Zustand gilt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AF\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/4fd12bff85b758729468c0cc1b3750b8229d3da3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.869ex; height:2.509ex;" alt="{\displaystyle AF\phi }" loading="lazy"> – man erreicht immer einen Zustand, in dem <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> gilt</li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AG\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/c97d0a96da3838cd8860cb08e50c6ca673f2a9b5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.955ex; height:2.509ex;" alt="{\displaystyle AG\phi }" loading="lazy"> – auf allen Pfaden gilt in jedem Zustand <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A[\phi U\psi ]}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/db501b7b98b121e02a244d11f4561599601c5760.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.718ex; height:2.843ex;" alt="{\displaystyle A[\phi U\psi ]}" loading="lazy"> – es gilt immer <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy"> bis zum ersten Auftreten von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }" loading="lazy"></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Semantik">Semantik</h2></div>

CTL Formeln werden über <a href="Transitionssystem" title="Transitionssystem">Transitionssysteme</a> definiert. Für eine gegebene Folge von Zuständen des Systems <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T(s_{0})=s_{0},s_{1},\ldots }">

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})=s_{0},s_{1},\ldots }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f198034e0699580f67c4969d967d0d6c64c3ef6e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:17.769ex; height:2.843ex;" alt="{\displaystyle T(s_{0})=s_{0},s_{1},\ldots }" loading="lazy"> (beginnend in Zustand <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle s_{0}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle s_{0}}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/25c32f35eb134d23b3c45f1c878d59b0a112ede4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.145ex; height:2.009ex;" alt="{\displaystyle s_{0}}" loading="lazy">) sind die Operatoren formal wie folgt definiert, dabei steht <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T(s_{0})\models \phi }">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/0299dec13b759dd4e345ee7e3d111df280d8b9be.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.281ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models \phi }" loading="lazy"> für <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle T(s_{0})}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/3d2d317336962677dcc9dd376d468dcab6ad1f35.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.59ex; height:2.843ex;" alt="{\displaystyle T(s_{0})}" loading="lazy"> erfüllt <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \phi }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/72b1f30316670aee6270a28334bdf4f5072cdde4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.385ex; height:2.509ex;" alt="{\displaystyle \phi }" loading="lazy">:

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models \neg \phi \quad \Leftrightarrow \quad T(s_{0})\not \models \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/66099fa6b29bc665df6b914813f85bc0a452d78d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:29.777ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models \neg \phi \quad \Leftrightarrow \quad T(s_{0})\not \models \phi }" loading="lazy"></li>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mrow>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models \phi \lor \psi \quad \Leftrightarrow \quad T(s_{0})\models \phi {\text{ oder }}T(s_{0})\models \psi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/37c52a63484b0d73378a0a503a8a14c9b575fda3.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:48.886ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models \phi \lor \psi \quad \Leftrightarrow \quad T(s_{0})\models \phi {\text{ oder }}T(s_{0})\models \psi }" loading="lazy"></li>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models EX\phi \quad \Leftrightarrow \quad T(s_{1})\models \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/e93d7cfcd835e2276f99d2141922bd7b68a1122c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:32.577ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models EX\phi \quad \Leftrightarrow \quad T(s_{1})\models \phi }" loading="lazy"></li>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models EG\phi \quad \Leftrightarrow \quad \forall i:T(s_{i})\models \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/75cdcd573cb7d89fd6a7ea7e69f6465cbfd3d51e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:36.201ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models EG\phi \quad \Leftrightarrow \quad \forall i:T(s_{i})\models \phi }" loading="lazy"></li>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle T(s_{0})\models \phi EU\psi \quad \Leftrightarrow \quad \exists k:T(s_{k})\models \psi \land \forall i<k:T(s_{i})\models \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1e5aae2c383fa91473954ce471a829c29bc2a8d1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:59.446ex; height:2.843ex;" alt="{\displaystyle T(s_{0})\models \phi EU\psi \quad \Leftrightarrow \quad \exists k:T(s_{k})\models \psi \land \forall i<k:T(s_{i})\models \phi }" loading="lazy"></li></ul>

Die oben genannten Umformungen erlauben es, Formeln ineinander umzuwandeln.

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg A\phi \equiv E\neg \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/93382106fc78b4dc8b3d03da8718c5fd0a317b81.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:12.489ex; height:2.509ex;" alt="{\displaystyle \neg A\phi \equiv E\neg \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg AF\phi \equiv EG\neg \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/18e2f03724a1739d0c69b4bb75f080ba1424c65b.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:16.056ex; height:2.509ex;" alt="{\displaystyle \neg AF\phi \equiv EG\neg \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg EF\phi \equiv AG\neg \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/25b3864276c430af2973d13420c63562972fa5a1.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:16.056ex; height:2.509ex;" alt="{\displaystyle \neg EF\phi \equiv AG\neg \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg AX\phi \equiv EX\neg \phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/778b6bd72e8747e61b47b3d7ed256376a6c77b30.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:16.449ex; height:2.509ex;" alt="{\displaystyle \neg AX\phi \equiv EX\neg \phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AG\phi \equiv \phi \land AXAG\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/f0364fe35455e99a8b8921b6e2b662ed69ce731e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.7ex; height:2.509ex;" alt="{\displaystyle AG\phi \equiv \phi \land AXAG\phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle EG\phi \equiv \phi \land EXEG\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/3f8a3c8d890e863d14685d05b2c47e1ff2ceb01a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.798ex; height:2.509ex;" alt="{\displaystyle EG\phi \equiv \phi \land EXEG\phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle AF\phi \equiv \phi \lor AXAF\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/ac867ff99f6db222225dd052ab3979c819036419.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.528ex; height:2.509ex;" alt="{\displaystyle AF\phi \equiv \phi \lor AXAF\phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle EF\phi \equiv \phi \lor EXEF\phi }</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/83c1396dd5043b477b86fcbef6a1e6936213e14f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:20.626ex; height:2.509ex;" alt="{\displaystyle EF\phi \equiv \phi \lor EXEF\phi }" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/04e432a4e05e0f27a955be8f1520f6746e653517.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:32.131ex; height:2.843ex;" alt="{\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}" loading="lazy"></li>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}</annotation>

</semantics>

</math><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/1e5839bd0d5c32f192612cb8ed45733343e15442.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:32.228ex; height:2.843ex;" alt="{\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}" loading="lazy"></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Literatur">Literatur</h2></div>

<ul><li>Clarke, Grumberg, Peled: Model Checking. MIT Press, 2000, ISBN 0-262-03270-8</li>

<li>Rohit Kapur: CTL for Test Information of Digital ICS. Springer, 2002, ISBN 978-1-4020-7293-2</li>

<li>B. Berard, Michel Bidoit, Alain Finkel: Systems and Software Verification. Model-checking Techniques and Tools. Springer, 2001, ISBN 3-540-41523-8</li>

<li>M. Huth and M. Ryan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge, 2004, ISBN 0-521-54310-X</li></ul></div><div><div class="zim-footer">

Dieser Artikel wurde von <a class="external text" title="Zuletzt bearbeitet am 2025-10-10" href="https://de.wikipedia.org/wiki/?title=Computation_Tree_Logic&oldid=260469036">Wikipedia</a> herausgegeben. Der Text ist unter <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de">Creative Commons Attribution-Share Alike 4.0</a> verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.

</div>

</div></div>

</div>

</main>

</div>

</body></html>